Issue2429.agda:8,17-28
Found a non-strict lambda where a irrelevant lambda was expected
when checking that the expression λ ..a → f a has type .A → B
